(* Author: Alexander Maletzky *)

section ‹Utilities›

theory Utils
  imports Main Well_Quasi_Orders.Almost_Full_Relations
begin

lemma subset_imageE_inj:
  assumes "B ⊆ f ` A"
  obtains C where "C ⊆ A" and "B = f ` C" and "inj_on f C"
proof -
  define g where "g = (λx. SOME a. a ∈ A ∧ f a = x)"
  have "g b ∈ A ∧ f (g b) = b" if "b ∈ B" for b
  proof -
    from that assms have "b ∈ f ` A" ..
    then obtain a where "a ∈ A" and "b = f a" ..
    hence "a ∈ A ∧ f a = b" by simp
    thus ?thesis unfolding g_def by (rule someI)
  qed
  hence 1: "⋀b. b ∈ B ⟹ g b ∈ A" and 2: "⋀b. b ∈ B ⟹ f (g b) = b" by simp_all
  let ?C = "g ` B"
  show ?thesis
  proof
    show "?C ⊆ A" by (auto intro: 1)
  next
    show "B = f ` ?C"
    proof (rule set_eqI)
      fix b
      show "b ∈ B ⟷ b ∈ f ` ?C"
      proof
        assume "b ∈ B"
        moreover from this have "f (g b) = b" by (rule 2)
        ultimately show "b ∈ f ` ?C" by force
      next
        assume "b ∈ f ` ?C"
        then obtain b' where "b' ∈ B" and "b = f (g b')" unfolding image_image ..
        moreover from this(1) have "f (g b') = b'" by (rule 2)
        ultimately show "b ∈ B" by simp
      qed
    qed
  next
    show "inj_on f ?C"
    proof
      fix x y
      assume "x ∈ ?C"
      then obtain bx where "bx ∈ B" and x: "x = g bx" ..
      moreover from this(1) have "f (g bx) = bx" by (rule 2)
      ultimately have *: "f x = bx" by simp
      assume "y ∈ ?C"
      then obtain "by" where "by ∈ B" and y: "y = g by" ..
      moreover from this(1) have "f (g by) = by" by (rule 2)
      ultimately have "f y = by" by simp
      moreover assume "f x = f y"
      ultimately have "bx = by" using * by simp
      thus "x = y" by (simp only: x y)
    qed
  qed
qed

lemma wfP_chain:
  assumes "¬(∃f. ∀i. r (f (Suc i)) (f i))"
  shows "wfP r"
proof -
  from assms wf_iff_no_infinite_down_chain[of "{(x, y). r x y}"] have "wf {(x, y). r x y}" by auto
  thus "wfP r" unfolding wfP_def .
qed

lemma transp_sequence:
  assumes "transp r" and "⋀i. r (seq (Suc i)) (seq i)" and "i < j"
  shows "r (seq j) (seq i)"
proof -
  have "⋀k. r (seq (i + Suc k)) (seq i)"
  proof -
    fix k::nat
    show "r (seq (i + Suc k)) (seq i)"
    proof (induct k)
      case 0
      from assms(2) have "r (seq (Suc i)) (seq i)" .
      thus ?case by simp
    next
      case (Suc k)
      note assms(1)
      moreover from assms(2) have "r (seq (Suc (Suc i + k))) (seq (Suc (i + k)))" by simp
      moreover have "r (seq (Suc (i + k))) (seq i)" using Suc.hyps by simp
      ultimately have "r (seq (Suc (Suc i + k))) (seq i)" by (rule transpD)
      thus ?case by simp
    qed
  qed
  hence "r (seq (i + Suc(j - i - 1))) (seq i)" .
  thus "r (seq j) (seq i)" using ‹i < j› by simp
qed

lemma almost_full_on_finite_subsetE:
  assumes "reflp P" and "almost_full_on P S"
  obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. P t s)"
proof -
  define crit where "crit = (λU s. s ∈ S ∧ (∀u∈U. ¬ P u s))"
  have critD: "s ∉ U" if "crit U s" for U s
  proof
    assume "s ∈ U"
    from ‹crit U s› have "∀u∈U. ¬ P u s" unfolding crit_def ..
    from this ‹s ∈ U› have "¬ P s s" ..
    moreover from assms(1) have "P s s" by (rule reflpD)
    ultimately show False ..
  qed
  define "fun"
    where "fun = (λU. (if (∃s. crit U s) then
                        insert (SOME s. crit U s) U
                      else
                        U
                      ))"
  define seq where "seq = rec_nat {} (λ_. fun)"
  have seq_Suc: "seq (Suc i) = fun (seq i)" for i by (simp add: seq_def)
  
  have seq_incr_Suc: "seq i ⊆ seq (Suc i)" for i by (auto simp add: seq_Suc fun_def)
  have seq_incr: "i ≤ j ⟹ seq i ⊆ seq j" for i j
  proof -
    assume "i ≤ j"
    hence "i = j ∨ i < j" by auto
    thus "seq i ⊆ seq j"
    proof
      assume "i = j"
      thus ?thesis by simp
    next
      assume "i < j"
      with _ seq_incr_Suc show ?thesis by (rule transp_sequence, simp add: transp_def)
    qed
  qed
  have sub: "seq i ⊆ S" for i
  proof (induct i, simp add: seq_def, simp add: seq_Suc fun_def, rule)
    fix i
    assume "Ex (crit (seq i))"
    hence "crit (seq i) (Eps (crit (seq i)))" by (rule someI_ex)
    thus "Eps (crit (seq i)) ∈ S" by (simp add: crit_def)
  qed
  have "∃i. seq (Suc i) = seq i"
  proof (rule ccontr, simp)
    assume "∀i. seq (Suc i) ≠ seq i"
    with seq_incr_Suc have "seq i ⊂ seq (Suc i)" for i by blast
    define seq1 where "seq1 = (λn. (SOME s. s ∈ seq (Suc n) ∧ s ∉ seq n))"
    have seq1: "seq1 n ∈ seq (Suc n) ∧ seq1 n ∉ seq n" for n unfolding seq1_def
    proof (rule someI_ex)
      from ‹seq n ⊂ seq (Suc n)› show "∃x. x ∈ seq (Suc n) ∧ x ∉ seq n" by blast
    qed
    have "seq1 i ∈ S" for i
    proof
      from seq1[of i] show "seq1 i ∈ seq (Suc i)" ..
    qed (fact sub)
    with assms(2) obtain a b where "a < b" and "P (seq1 a) (seq1 b)" by (rule almost_full_onD)
    from ‹a < b› have "Suc a ≤ b" by simp
    from seq1 have "seq1 a ∈ seq (Suc a)" ..
    also from ‹Suc a ≤ b› have "... ⊆ seq b" by (rule seq_incr)
    finally have "seq1 a ∈ seq b" .
    from seq1 have "seq1 b ∈ seq (Suc b)" and "seq1 b ∉ seq b" by blast+
    hence "crit (seq b) (seq1 b)" by (simp add: seq_Suc fun_def someI split: if_splits)
    hence "∀u∈seq b. ¬ P u (seq1 b)" by (simp add: crit_def)
    from this ‹seq1 a ∈ seq b› have "¬ P (seq1 a) (seq1 b)" ..
    from this ‹P (seq1 a) (seq1 b)› show False ..
  qed
  then obtain i where "seq (Suc i) = seq i" ..
  show ?thesis
  proof
    show "finite (seq i)" by (induct i, simp_all add: seq_def fun_def)
  next
    fix s
    assume "s ∈ S"
    let ?s = "Eps (crit (seq i))"
    show "∃t∈seq i. P t s"
    proof (rule ccontr, simp)
      assume "∀t∈seq i. ¬ P t s"
      with ‹s ∈ S› have "crit (seq i) s" by (simp only: crit_def)
      hence "crit (seq i) ?s" and eq: "seq (Suc i) = insert ?s (seq i)"
        by (auto simp add: seq_Suc fun_def intro: someI)
      from this(1) have "?s ∉ seq i" by (rule critD)
      hence "seq (Suc i) ≠ seq i" unfolding eq by blast
      from this ‹seq (Suc i) = seq i› show False ..
    qed
  qed (fact sub)
qed

subsection ‹Lists›

lemma map_upt: "map (λi. f (xs ! i)) [0..<length xs] = map f xs"
  by (auto intro: nth_equalityI)

lemma map_upt_zip:
  assumes "length xs = length ys"
  shows "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] = map (λ(x, y). f x y) (zip xs ys)" (is "?l = ?r")
proof -
  have len_l: "length ?l = length ys" by simp
  from assms have len_r: "length ?r = length ys" by simp
  show ?thesis
  proof (simp only: list_eq_iff_nth_eq len_l len_r, rule, rule, intro allI impI)
    fix i
    assume "i < length ys"
    hence "i < length ?l" and "i < length ?r" by (simp_all only: len_l len_r)
    thus "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] ! i = map (λ(x, y). f x y) (zip xs ys) ! i"
      by simp
  qed
qed

lemma distinct_sorted_wrt_irrefl:
  assumes "irreflp rel" and "transp rel" and "sorted_wrt rel xs"
  shows "distinct xs"
  using assms(3)
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  from Cons(2) have "sorted_wrt rel xs" and *: "∀y∈set xs. rel x y"
    by (simp_all)
  from this(1) have "distinct xs" by (rule Cons(1))
  show ?case
  proof (simp add: ‹distinct xs›, rule)
    assume "x ∈ set xs"
    with * have "rel x x" ..
    with assms(1) show False by (simp add: irreflp_def)
  qed
qed

lemma distinct_sorted_wrt_imp_sorted_wrt_strict:
  assumes "distinct xs" and "sorted_wrt rel xs"
  shows "sorted_wrt (λx y. rel x y ∧ ¬ x = y) xs"
  using assms
proof (induct xs)
  case Nil
  show ?case by simp
next
  case step: (Cons x xs)
  show ?case
  proof (cases "xs")
    case Nil
    thus ?thesis by simp
  next
    case (Cons y zs)
    from step(2) have "x ≠ y" and 1: "distinct (y # zs)" by (simp_all add: Cons)
    from step(3) have "rel x y" and 2: "sorted_wrt rel (y # zs)" by (simp_all add: Cons)
    from 1 2 have "sorted_wrt (λx y. rel x y ∧ x ≠ y) (y # zs)" by (rule step(1)[simplified Cons])
    with ‹x ≠ y› ‹rel x y› show ?thesis using step.prems by (auto simp: Cons)
  qed
qed

lemma sorted_wrt_distinct_set_unique:
  assumes "antisymp rel"
  assumes "sorted_wrt rel xs" "distinct xs" "sorted_wrt rel ys" "distinct ys" "set xs = set ys"
  shows "xs = ys"
proof -
  from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  from assms(2-6) show ?thesis
  proof(induct rule:list_induct2[OF 1])
    case 1
    show ?case by simp
  next
    case (2 x xs y ys)
    from 2(4) have "x ∉ set xs" and "distinct xs" by simp_all
    from 2(6) have "y ∉ set ys" and "distinct ys" by simp_all
    have "x = y"
    proof (rule ccontr)
      assume "x ≠ y"
      from 2(3) have "∀z∈set xs. rel x z" by (simp)
      moreover from ‹x ≠ y› have "y ∈ set xs" using 2(7) by auto
      ultimately have *: "rel x y" ..
      from 2(5) have "∀z∈set ys. rel y z" by (simp)
      moreover from ‹x ≠ y› have "x ∈ set ys" using 2(7) by auto
      ultimately have "rel y x" ..
      with assms(1) * have "x = y" by (rule antisympD)
      with ‹x ≠ y› show False ..
    qed
    from 2(3) have "sorted_wrt rel xs" by (simp)
    moreover note ‹distinct xs›
    moreover from 2(5) have "sorted_wrt rel ys" by (simp)
    moreover note ‹distinct ys›
    moreover from 2(7) ‹x ∉ set xs› ‹y ∉ set ys› have "set xs = set ys" by (auto simp add: ‹x = y›)
    ultimately have "xs = ys" by (rule 2(2))
    with ‹x = y› show ?case by simp
  qed
qed

lemma sorted_wrt_refl_nth_mono:
  assumes "reflp P" and "sorted_wrt P xs" and "i ≤ j" and "j < length xs"
  shows "P (xs ! i) (xs ! j)"
proof (cases "i < j")
  case True
  from assms(2) this assms(4) show ?thesis by (rule sorted_wrt_nth_less)
next
  case False
  with assms(3) have "i = j" by simp
  from assms(1) show ?thesis unfolding ‹i = j› by (rule reflpD)
qed

fun merge_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
  "merge_wrt _ xs [] = xs"|
  "merge_wrt rel [] ys = ys"|
  "merge_wrt rel (x # xs) (y # ys) =
    (if x = y then
      y # (merge_wrt rel xs ys)
    else if rel x y then
      x # (merge_wrt rel xs (y # ys))
    else
      y # (merge_wrt rel (x # xs) ys)
    )"

lemma set_merge_wrt: "set (merge_wrt rel xs ys) = set xs ∪ set ys"
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  show ?case by simp
next
  case (2 rel y ys)
  show ?case by simp
next
  case (3 rel x xs y ys)
  show ?case
  proof (cases "x = y")
    case True
    thus ?thesis by (simp add: 3(1))
  next
    case False
    show ?thesis
    proof (cases "rel x y")
      case True
      with ‹x ≠ y› show ?thesis by (simp add: 3(2) insert_commute)
    next
      case False
      with ‹x ≠ y› show ?thesis by (simp add: 3(3))
    qed
  qed
qed

lemma sorted_merge_wrt:
  assumes "transp rel" and "⋀x y. x ≠ y ⟹ rel x y ∨ rel y x"
    and "sorted_wrt rel xs" and "sorted_wrt rel ys"
  shows "sorted_wrt rel (merge_wrt rel xs ys)"
  using assms
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  from 1(3) show ?case by simp
next
  case (2 rel y ys)
  from 2(4) show ?case by simp
next
  case (3 rel x xs y ys)
  show ?case
  proof (cases "x = y")
    case True
    show ?thesis
    proof (auto simp add: True)
      fix z
      assume "z ∈ set (merge_wrt rel xs ys)"
      hence "z ∈ set xs ∪ set ys" by (simp only: set_merge_wrt)
      thus "rel y z"
      proof
        assume "z ∈ set xs"
        with 3(6) show ?thesis by (simp add: True)
      next
        assume "z ∈ set ys"
        with 3(7) show ?thesis by (simp)
      qed
    next
      note True 3(4, 5)
      moreover from 3(6) have "sorted_wrt rel xs" by (simp)
      moreover from 3(7) have "sorted_wrt rel ys" by (simp)
      ultimately show "sorted_wrt rel (merge_wrt rel xs ys)" by (rule 3(1))
    qed
  next
    case False
    show ?thesis
    proof (cases "rel x y")
      case True
      show ?thesis
      proof (auto simp add: False True)
        fix z
        assume "z ∈ set (merge_wrt rel xs (y # ys))"
        hence "z ∈ insert y (set xs ∪ set ys)" by (simp add: set_merge_wrt)
        thus "rel x z"
        proof
          assume "z = y"
          with True show ?thesis by simp
        next
          assume "z ∈ set xs ∪ set ys"
          thus ?thesis
          proof
            assume "z ∈ set xs"
            with 3(6) show ?thesis by (simp)
          next
            assume "z ∈ set ys"
            with 3(7) have "rel y z" by (simp)
            with 3(4) True show ?thesis by (rule transpD)
          qed
        qed
      next
        note False True 3(4, 5)
        moreover from 3(6) have "sorted_wrt rel xs" by (simp)
        ultimately show "sorted_wrt rel (merge_wrt rel xs (y # ys))" using 3(7) by (rule 3(2))
      qed
    next
      assume "¬ rel x y"
      from ‹x ≠ y› have "rel x y ∨ rel y x" by (rule 3(5))
      with ‹¬ rel x y› have *: "rel y x" by simp
      show ?thesis
      proof (auto simp add: False ‹¬ rel x y›)
        fix z
        assume "z ∈ set (merge_wrt rel (x # xs) ys)"
        hence "z ∈ insert x (set xs ∪ set ys)" by (simp add: set_merge_wrt)
        thus "rel y z"
        proof
          assume "z = x"
          with * show ?thesis by simp
        next
          assume "z ∈ set xs ∪ set ys"
          thus ?thesis
          proof
            assume "z ∈ set xs"
            with 3(6) have "rel x z" by (simp)
            with 3(4) * show ?thesis by (rule transpD)
          next
            assume "z ∈ set ys"
            with 3(7) show ?thesis by (simp)
          qed
        qed
      next
        note False ‹¬ rel x y› 3(4, 5, 6)
        moreover from 3(7) have "sorted_wrt rel ys" by (simp)
        ultimately show "sorted_wrt rel (merge_wrt rel (x # xs) ys)" by (rule 3(3))
      qed
    qed
  qed
qed

lemma set_fold:
  assumes "⋀x ys. set (f (g x) ys) = set (g x) ∪ set ys"
  shows "set (fold (λx. f (g x)) xs ys) = (⋃x∈set xs. set (g x)) ∪ set ys"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have eq: "set (fold (λx. f (g x)) xs (f (g x) ys)) = (⋃x∈set xs. set (g x)) ∪ set (f (g x) ys)"
    by (rule Cons)
  show ?case by (simp add: o_def assms set_merge_wrt eq ac_simps)
qed

subsection ‹Sums and Products›

lemma additive_implies_homogenous:
  assumes "⋀x y. f (x + y) = f x + ((f (y::'a::monoid_add))::'b::cancel_comm_monoid_add)"
  shows "f 0 = 0"
proof -
  have "f (0 + 0) = f 0 + f 0" by (rule assms)
  hence "f 0 = f 0 + f 0" by simp
  thus "f 0 = 0" by simp
qed

lemma fun_sum_commute:
  assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
  shows "f (sum g A) = (∑a∈A. f (g a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    thus ?case by (simp add: assms(1))
  next
    case step: (insert a A)
    show ?case by (simp add: sum.insert[OF step(1) step(2)] assms(2) step(3))
  qed
next
  case False
  thus ?thesis by (simp add: assms(1))
qed

lemma fun_sum_commute_canc:
  assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
  shows "f (sum g A) = (∑a∈A. f (g a))"
  by (rule fun_sum_commute, rule additive_implies_homogenous, fact+)

lemma fun_sum_list_commute:
  assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
  shows "f (sum_list xs) = sum_list (map f xs)"
proof (induct xs)
  case Nil
  thus ?case by (simp add: assms(1))
next
  case (Cons x xs)
  thus ?case by (simp add: assms(2))
qed

lemma fun_sum_list_commute_canc:
  assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
  shows "f (sum_list xs) = sum_list (map f xs)"
  by (rule fun_sum_list_commute, rule additive_implies_homogenous, fact+)

lemma sum_set_upt_eq_sum_list: "(∑i = m..<n. f i) = (∑i←[m..<n]. f i)"
  using sum_set_upt_conv_sum_list_nat by auto

lemma sum_list_upt: "(∑i←[0..<(length xs)]. f (xs ! i)) = (∑x←xs. f x)"
  by (simp only: map_upt)

lemma sum_list_upt_zip:
  assumes "length xs = length ys"
  shows "(∑i←[0..<(length ys)]. f (xs ! i) (ys ! i)) = (∑(x, y)←(zip xs ys). f x y)"
  by (simp only: map_upt_zip[OF assms])

lemma sum_list_zeroI:
  assumes "set xs ⊆ {0}"
  shows "sum_list xs = 0"
  using assms by (induct xs, auto)

lemma fun_prod_commute:
  assumes "f 1 = 1" and "⋀x y. f (x * y) = f x * f y"
  shows "f (prod g A) = (∏a∈A. f (g a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    thus ?case by (simp add: assms(1))
  next
    case step: (insert a A)
    show ?case by (simp add: prod.insert[OF step(1) step(2)] assms(2) step(3))
  qed
next
  case False
  thus ?thesis by (simp add: assms(1))
qed

end (* theory *)

(* Author: Andreas Lochbihler, ETH Zurich
   Author: Florian Haftmann, TU Muenchen
*)

section ‹An abstract type for multivariate polynomials›

theory MPoly_Type
imports "HOL-Library.Poly_Mapping"
begin

subsection ‹Abstract type definition›

typedef (overloaded) 'a mpoly =
  "UNIV :: ((nat ⇒⇩0 nat) ⇒⇩0 'a::zero) set"
  morphisms mapping_of MPoly
 ..

setup_lifting type_definition_mpoly

(* these theorems are automatically generated by setup_lifting... *)
thm mapping_of_inverse   thm MPoly_inverse
thm mapping_of_inject    thm MPoly_inject
thm mapping_of_induct    thm MPoly_induct
thm mapping_of_cases     thm MPoly_cases


subsection ‹Additive structure›

instantiation mpoly :: (zero) zero
begin

lift_definition zero_mpoly :: "'a mpoly"
  is "0 :: (nat ⇒⇩0 nat) ⇒⇩0 'a" .

instance ..

end

instantiation mpoly :: (monoid_add) monoid_add
begin

lift_definition plus_mpoly :: "'a mpoly ⇒ 'a mpoly ⇒ 'a mpoly"
  is "Groups.plus :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .

instance
  by intro_classes (transfer, simp add: fun_eq_iff add.assoc)+

end

instance mpoly :: (comm_monoid_add) comm_monoid_add
  by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+

instantiation mpoly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
begin

lift_definition minus_mpoly :: "'a mpoly ⇒ 'a mpoly ⇒ 'a mpoly"
  is "Groups.minus :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .

instance
  by intro_classes (transfer, simp add: fun_eq_iff diff_diff_add)+

end

instantiation mpoly :: (ab_group_add) ab_group_add
begin

lift_definition uminus_mpoly :: "'a mpoly ⇒ 'a mpoly"
  is "Groups.uminus :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .


instance
  by intro_classes (transfer, simp add: fun_eq_iff add_uminus_conv_diff)+

end


subsection ‹Multiplication by a coefficient›
(* ?do we need inc_power on abstract polynomials? *)

lift_definition smult :: "'a::{times,zero} ⇒ 'a mpoly ⇒ 'a mpoly"
  is "λa. Poly_Mapping.map (Groups.times a) :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .

(* left lemmas in subsection ‹Pseudo-division of polynomials›,
   because I couldn't disentangle them and the notion of monomials. *)

subsection ‹Multiplicative structure›

instantiation mpoly :: (zero_neq_one) zero_neq_one
begin

lift_definition one_mpoly :: "'a mpoly"
  is "1 :: ((nat ⇒⇩0 nat) ⇒⇩0 'a)" .

instance
  by intro_classes (transfer, simp)

end

instantiation mpoly :: (semiring_0) semiring_0
begin

lift_definition times_mpoly :: "'a mpoly ⇒ 'a mpoly ⇒ 'a mpoly"
  is "Groups.times :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .

instance
  by intro_classes (transfer, simp add: algebra_simps)+

end

instance mpoly :: (comm_semiring_0) comm_semiring_0
  by intro_classes (transfer, simp add: algebra_simps)+

instance mpoly :: (semiring_0_cancel) semiring_0_cancel
  ..

instance mpoly :: (comm_semiring_0_cancel) comm_semiring_0_cancel
  ..

instance mpoly :: (semiring_1) semiring_1
  by intro_classes (transfer, simp)+

instance mpoly :: (comm_semiring_1) comm_semiring_1
  by intro_classes (transfer, simp)+

instance mpoly :: (semiring_1_cancel) semiring_1_cancel
  ..

(*instance mpoly :: (comm_semiring_1_cancel) comm_semiring_1_cancel
  .. FIXME unclear whether this holds *)

instance mpoly :: (ring) ring
  ..

instance mpoly :: (comm_ring) comm_ring
  ..

instance mpoly :: (ring_1) ring_1
  ..

instance mpoly :: (comm_ring_1) comm_ring_1
  ..


subsection ‹Monomials›

text ‹
  Terminology is not unique here, so we use the notions as follows:
  A "monomial" and a "coefficient" together give a "term".
  These notions are significant in connection with "leading",
  "leading term", "leading coefficient" and "leading monomial",
  which all rely on a monomial order.
›

lift_definition monom :: "(nat ⇒⇩0 nat) ⇒ 'a::zero ⇒ 'a mpoly"
  is "Poly_Mapping.single :: (nat ⇒⇩0 nat) ⇒ _" .

lemma mapping_of_monom [simp]:
  "mapping_of (monom m a) = Poly_Mapping.single m a"
  by(fact monom.rep_eq)

lemma monom_zero [simp]:
  "monom 0 0 = 0"
  by transfer simp

lemma monom_one [simp]:
  "monom 0 1 = 1"
  by transfer simp

lemma monom_add:
  "monom m (a + b) = monom m a + monom m b"
  by transfer (simp add: single_add)

lemma monom_uminus:
  "monom m (- a) = - monom m a"
  by transfer (simp add: single_uminus)

lemma monom_diff:
  "monom m (a - b) = monom m a - monom m b"
  by transfer (simp add: single_diff)

lemma monom_numeral [simp]:
  "monom 0 (numeral n) = numeral n"
  by (induct n) (simp_all only: numeral.simps numeral_add monom_zero monom_one monom_add)

lemma monom_of_nat [simp]:
  "monom 0 (of_nat n) = of_nat n"
  by (induct n) (simp_all add: monom_add)

lemma of_nat_monom:
  "of_nat = monom 0 ∘ of_nat"
  by (simp add: fun_eq_iff)

lemma inj_monom [iff]:
  "inj (monom m)"
proof (rule injI, transfer)
  fix a b :: 'a and m :: "nat ⇒⇩0 nat"
  assume "Poly_Mapping.single m a = Poly_Mapping.single m b"
  with injD [of "Poly_Mapping.single m" a b]
  show "a = b" by simp
qed

lemma mult_monom: "monom x a * monom y b = monom (x + y) (a * b)"
  by transfer' (simp add: Poly_Mapping.mult_single)

instance mpoly :: (semiring_char_0) semiring_char_0
  by intro_classes (auto simp add: of_nat_monom inj_of_nat intro: inj_compose)

instance mpoly :: (ring_char_0) ring_char_0
  ..

lemma monom_of_int [simp]:
  "monom 0 (of_int k) = of_int k"
  apply (cases k)
  apply simp_all
  unfolding monom_diff monom_uminus
  apply simp
  done

subsection ‹Constants and Indeterminates›

text ‹Embedding of indeterminates and constants in type-class polynomials,
  can be used as constructors.›

definition Var⇩0 :: "'a ⇒ ('a ⇒⇩0 nat) ⇒⇩0 'b::{one,zero}" where
  "Var⇩0 n ≡ Poly_Mapping.single (Poly_Mapping.single n 1) 1"
definition Const⇩0 :: "'b ⇒ ('a ⇒⇩0 nat) ⇒⇩0 'b::zero" where "Const⇩0 c ≡ Poly_Mapping.single 0 c"

lemma Const⇩0_one: "Const⇩0 1 = 1"
  by (simp add: Const⇩0_def)

lemma Const⇩0_numeral: "Const⇩0 (numeral x) = numeral x"
  by (auto intro!: poly_mapping_eqI simp: Const⇩0_def lookup_numeral)

lemma Const⇩0_minus: "Const⇩0 (- x) = - Const⇩0 x"
  by (simp add: Const⇩0_def single_uminus)

lemma Const⇩0_zero: "Const⇩0 0 = 0"
  by (auto intro!: poly_mapping_eqI simp: Const⇩0_def)

lemma Var⇩0_power: "Var⇩0 v ^ n = Poly_Mapping.single (Poly_Mapping.single v n) 1"
  by (induction n) (auto simp: Var⇩0_def mult_single single_add[symmetric])

lift_definition Var::"nat ⇒ 'b::{one,zero} mpoly" is Var⇩0 .
lift_definition Const::"'b::zero ⇒ 'b mpoly" is Const⇩0 .


subsection ‹Integral domains›

instance mpoly :: (ring_no_zero_divisors) ring_no_zero_divisors
  by intro_classes (transfer, simp)

instance mpoly :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors
  ..

instance mpoly :: (idom) idom
  ..


subsection ‹Monom coefficient lookup›

definition coeff :: "'a::zero mpoly ⇒ (nat ⇒⇩0 nat) ⇒ 'a"
where
  "coeff p = Poly_Mapping.lookup (mapping_of p)"


subsection ‹Insertion morphism›

definition insertion_fun_natural :: "(nat ⇒ 'a) ⇒ ((nat ⇒ nat) ⇒ 'a) ⇒ 'a::comm_semiring_1"
where
  "insertion_fun_natural f p = (∑m. p m * (∏v. f v ^ m v))"

definition insertion_fun :: "(nat ⇒ 'a) ⇒ ((nat ⇒⇩0 nat) ⇒ 'a) ⇒ 'a::comm_semiring_1"
where
  "insertion_fun f p = (∑m. p m * (∏v. f v ^ Poly_Mapping.lookup m v))"

text ‹N.b. have been unable to relate this to @{const insertion_fun_natural} using lifting!›

lift_definition insertion_aux :: "(nat ⇒ 'a) ⇒ ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ 'a::comm_semiring_1"
  is "insertion_fun" .

lift_definition insertion :: "(nat ⇒ 'a) ⇒ 'a mpoly ⇒ 'a::comm_semiring_1"
  is "insertion_aux" .

lemma aux:
  "Poly_Mapping.lookup f = (λ_. 0) ⟷ f = 0"
  apply transfer apply simp done

lemma insertion_trivial [simp]:
  "insertion (λ_. 0) p = coeff p 0"
proof -
  { fix f :: "(nat ⇒⇩0 nat) ⇒⇩0 'a"
    have "insertion_aux (λ_. 0) f = Poly_Mapping.lookup f 0"
      apply (simp add: insertion_aux_def insertion_fun_def power_Sum_any [symmetric])
      apply (simp add: zero_power_eq mult_when aux)
      done
  }
  then show ?thesis by (simp add: coeff_def insertion_def)
qed

lemma insertion_zero [simp]:
  "insertion f 0 = 0"
  by transfer (simp add: insertion_aux_def insertion_fun_def)

lemma insertion_fun_add:
  fixes f p q
  shows "insertion_fun f (Poly_Mapping.lookup (p + q)) =
    insertion_fun f (Poly_Mapping.lookup p) +
      insertion_fun f (Poly_Mapping.lookup q)"
  unfolding insertion_fun_def
  apply (subst Sum_any.distrib [symmetric])
  apply (simp_all add: plus_poly_mapping.rep_eq algebra_simps)
  apply (rule finite_mult_not_eq_zero_rightI)
  apply simp
  apply (rule finite_mult_not_eq_zero_rightI)
  apply simp
  done

lemma insertion_add:
  "insertion f (p + q) = insertion f p + insertion f q"
  by transfer (simp add: insertion_aux_def insertion_fun_add)

lemma insertion_one [simp]:
  "insertion f 1 = 1"
  by transfer (simp add: insertion_aux_def insertion_fun_def one_poly_mapping.rep_eq when_mult)

lemma insertion_fun_mult:
  fixes f p q
  shows "insertion_fun f (Poly_Mapping.lookup (p * q)) =
    insertion_fun f (Poly_Mapping.lookup p) *
      insertion_fun f (Poly_Mapping.lookup q)"
proof -
  { fix m :: "nat ⇒⇩0 nat"
    have "finite {v. Poly_Mapping.lookup m v ≠ 0}"
      by simp
    then have "finite {v. f v ^ Poly_Mapping.lookup m v ≠ 1}"
      by (rule rev_finite_subset) (auto intro: ccontr)
  }
  moreover define g where "g m = (∏v. f v ^ Poly_Mapping.lookup m v)" for m
  ultimately have *: "⋀a b. g (a + b) = g a * g b"
    by (simp add: plus_poly_mapping.rep_eq power_add Prod_any.distrib)
  have bij: "bij (λ(l, n, m). (m, l, n))"
    by (auto intro!: bijI injI simp add: image_def)
  let ?P = "{l. Poly_Mapping.lookup p l ≠ 0}"
  let ?Q = "{n. Poly_Mapping.lookup q n ≠ 0}"
  let ?PQ = "{l + n | l n. l ∈ Poly_Mapping.keys p ∧ n ∈ Poly_Mapping.keys q}"
  have "finite {l + n | l n. Poly_Mapping.lookup p l ≠ 0 ∧ Poly_Mapping.lookup q n ≠ 0}"
    by (rule finite_not_eq_zero_sumI) simp_all
  then have fin_PQ: "finite ?PQ"
    by (simp add: in_keys_iff)
  have "(∑m. Poly_Mapping.lookup (p * q) m * g m) =
    (∑m. (∑l. Poly_Mapping.lookup p l * (∑n. Poly_Mapping.lookup q n when m = l + n)) * g m)"
    by (simp add: times_poly_mapping.rep_eq prod_fun_def)
  also have "… = (∑m. (∑l. (∑n. g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)))"
    apply (subst Sum_any_left_distrib)
    apply (auto intro: finite_mult_not_eq_zero_rightI)
    apply (subst Sum_any_right_distrib)
    apply (auto intro: finite_mult_not_eq_zero_rightI)
    apply (subst Sum_any_left_distrib)
    apply (auto intro: finite_mult_not_eq_zero_leftI)
    apply (simp add: ac_simps mult_when)
    done
  also have "… = (∑m. (∑(l, n). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n))"
    apply (subst (2) Sum_any.cartesian_product [of "?P × ?Q"])
    apply (auto dest!: mult_not_zero)
    done
  also have "… = (∑(m, l, n). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)"
    apply (subst Sum_any.cartesian_product [of "?PQ × (?P × ?Q)"])
      apply (auto dest!: mult_not_zero simp add: fin_PQ)
    apply (auto simp: in_keys_iff)
    done
  also have "… = (∑(l, n, m). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)"
    using bij by (rule Sum_any.reindex_cong [of "λ(l, n, m). (m, l, n)"]) (simp add: fun_eq_iff)
  also have "… = (∑(l, n). ∑m. g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)"
    apply (subst Sum_any.cartesian_product2 [of "(?P × ?Q) × ?PQ"])
    apply (auto dest!: mult_not_zero simp add: fin_PQ )
    apply (auto simp: in_keys_iff)
    done
  also have "… = (∑(l, n). (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))"
    by (simp add: *)
  also have "… = (∑l. ∑n. (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))"
    apply (subst Sum_any.cartesian_product [of "?P × ?Q"])
    apply (auto dest!: mult_not_zero)
    done
  also have "… = (∑l. ∑n. (Poly_Mapping.lookup p l * g l) * (Poly_Mapping.lookup q n * g n))"
    by (simp add: ac_simps)
  also have "… =
    (∑m. Poly_Mapping.lookup p m * g m) *
    (∑m. Poly_Mapping.lookup q m * g m)"
    by (rule Sum_any_product [symmetric]) (auto intro: finite_mult_not_eq_zero_rightI)
  finally show ?thesis by (simp add: insertion_fun_def g_def)
qed

lemma insertion_mult:
  "insertion f (p * q) = insertion f p * insertion f q"
  by transfer (simp add: insertion_aux_def insertion_fun_mult)


subsection ‹Degree›

lift_definition degree :: "'a::zero mpoly ⇒ nat ⇒ nat"
is "λp v. Max (insert 0 ((λm. Poly_Mapping.lookup m v) ` Poly_Mapping.keys p))" .


lift_definition total_degree :: "'a::zero mpoly ⇒ nat"
is "λp. Max (insert 0 ((λm. sum (Poly_Mapping.lookup m) (Poly_Mapping.keys m)) ` Poly_Mapping.keys p))" .

lemma degree_zero [simp]:
  "degree 0 v = 0"
  by transfer simp

lemma total_degree_zero [simp]:
  "total_degree 0 = 0"
  by transfer simp
(*
value [code] "total_degree (0 :: int mpoly)" (***)
*)

lemma degree_one [simp]:
  "degree 1 v = 0"
  by transfer simp

lemma total_degree_one [simp]:
  "total_degree 1 = 0"
  by transfer simp

subsection ‹Pseudo-division of polynomials›

lemma smult_conv_mult: "smult s p = monom 0 s * p"
by transfer (simp add: mult_map_scale_conv_mult)

lemma smult_monom [simp]:
  fixes c :: "_ :: mult_zero"
  shows "smult c (monom x c') = monom x (c * c')"
by transfer simp

lemma smult_0 [simp]:
  fixes p :: "_ :: mult_zero mpoly"
  shows "smult 0 p = 0"
by transfer(simp add: map_eq_zero_iff)

lemma mult_smult_left: "smult s p * q = smult s (p * q)"
by(simp add: smult_conv_mult mult.assoc)

lift_definition sdiv :: "'a::euclidean_ring ⇒ 'a mpoly ⇒ 'a mpoly"
  is "λa. Poly_Mapping.map (λb. b div a) :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _"
.
text ‹
  \qt{Polynomial division} is only possible on univariate polynomials ‹K[x]›
  over a field ‹K›, all other kinds of polynomials only allow pseudo-division
  [1]p.40/41":

  ‹∀x y :: 'a mpoly. y ≠ 0 ⇒ ∃a q r. smult a x = q * y + r›

  The introduction of pseudo-division below generalises @{file ‹~~/src/HOL/Computational_Algebra/Polynomial.thy›}.
  [1] Winkler, Polynomial Algorithms, 1996.
  The generalisation raises issues addressed by Wenda Li and commented below.
  Florian replied to the issues conjecturing, that the abstract mpoly needs not
  be aware of the issues, in case these are only concerned with executability.
›

definition pseudo_divmod_rel
  :: "'a::euclidean_ring => 'a mpoly => 'a mpoly => 'a mpoly => 'a mpoly => bool"
where
  "pseudo_divmod_rel a x y q r ⟷
    smult a x = q * y + r ∧ (if y = 0 then q = 0 else r = 0 ∨ degree r < degree y)"
(* the notion of degree resigns a main variable in multivariate polynomials;
   also, there are infinitely many tuples (a,q,r) such that a x = q y + r *)

definition pdiv :: "'a::euclidean_ring mpoly ⇒ 'a mpoly ⇒ ('a × 'a mpoly)" (infixl "pdiv" 70)
where
  "x pdiv y = (THE (a, q). ∃r. pseudo_divmod_rel a x y q r)"

definition pmod :: "'a::euclidean_ring mpoly ⇒ 'a mpoly ⇒ 'a mpoly" (infixl "pmod" 70)
where
  "x pmod y = (THE r. ∃a q. pseudo_divmod_rel a x y q r)"

definition pdivmod :: "'a::euclidean_ring mpoly ⇒ 'a mpoly ⇒ ('a × 'a mpoly) × 'a mpoly"
where
  "pdivmod p q = (p pdiv q, p pmod q)"

(* "_code" seems inappropriate, since "THE" in definitions pdiv and pmod is not unique,
   see comment to definition pseudo_divmod_rel; so this cannot be executable ... *)
lemma pdiv_code:
  "p pdiv q = fst (pdivmod p q)"
  by (simp add: pdivmod_def)

lemma pmod_code:
  "p pmod q = snd (pdivmod p q)"
  by (simp add: pdivmod_def)

(*TODO ERROR: Ambiguous input produces n parse trees ???...*)
definition div :: "'a::{euclidean_ring,field} mpoly ⇒ 'a mpoly ⇒ 'a mpoly" (infixl "div" 70)
where
  "x div y = (THE q'. ∃a q r. (pseudo_divmod_rel a x y q r) ∧ (q' = smult (inverse a) q))"

definition mod :: "'a::{euclidean_ring,field} mpoly ⇒ 'a mpoly ⇒ 'a mpoly" (infixl "mod" 70)
where
  "x mod y = (THE r'. ∃a q r. (pseudo_divmod_rel a x y q r) ∧ (r' = smult (inverse a) r))"

definition divmod :: "'a::{euclidean_ring,field} mpoly ⇒ 'a mpoly ⇒ 'a mpoly × 'a mpoly"
where
  "divmod p q = (p div q, p mod q)"

lemma div_poly_code:
  "p div q = fst (divmod p q)"
  by (simp add: divmod_def)

lemma mod_poly_code:
  "p mod q = snd (divmod p q)"
  by (simp add: divmod_def)

subsection ‹Primitive poly, etc›

lift_definition coeffs :: "'a :: zero mpoly ⇒ 'a set"
is "Poly_Mapping.range :: ((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ _" .

lemma finite_coeffs [simp]: "finite (coeffs p)"
by transfer simp

text ‹[1]p.82
  A "primitive'" polynomial has coefficients with GCD equal to 1.
  A polynomial is factored into "content" and "primitive part"
  for many different purposes.›

definition primitive :: "'a::{euclidean_ring,semiring_Gcd} mpoly ⇒ bool"
where
  "primitive p ⟷ Gcd (coeffs p) = 1"

definition content_primitive :: "'a::{euclidean_ring,GCD.Gcd} mpoly ⇒ 'a × 'a mpoly"
where
  "content_primitive p = (
    let d = Gcd (coeffs p)
    in (d, sdiv d p))"

value "let p = M [1,2,3] (4::int) + M [2,0,4] 6 + M [2,0,5] 8
  in content_primitive p"


end